es:event_system{i:l}, l:IdLnk, tg:Id, L:(Knd List). sframe-p(es; l; tg; L)  prop{i:l} 

latex

Definitions	P  Q, A c B, t  T, guard(T), P  Q, x:A. B(x), event_system{i:l}, IdLnk, Id, Knd, b, es-sender(es; e), es-kind(es; e), (x  l), rcv(l,tg), prop{i:l}, es-E(es), sframe-p(es; l; tg; L)
Lemmas	es-E wf, rcv wf, l member wf, es-kind wf, es-sender wf, Knd wf, Id wf, IdLnk wf, event system wf, es-kind-rcv